package arlab.formulae.tests
import arlab.formulae._
import arlab.formulae.transformations._
object Main {
    def main (args: Array[String]) = {
        val a = Not(And(Or(Or(BooleanVariable("a"),BooleanVariable("b")),Not(BooleanVariable("c"))),Or(Or(Not(BooleanVariable("a")),BooleanVariable("d")),Not(BooleanVariable("g")))))
        println("normal:")
        println(a)        
        println("nnf:")
        println(Transformations.nnf(a))
        println("cnf:")
        println(Transformations.cnf(a))
        println("simple cnf:")
        println(Transformations.simplify(Transformations.cnf(a)))
        
        val b = Not(Not(Not(BooleanVariable("a"))))
        println("normal:")
        println(b)
        println("nnf:")
        println(Transformations.nnf(b))
        println("cnf:")
        println(Transformations.cnf(b))
        
        val c = Or(BooleanVariable("a"),Not(And(BooleanVariable("b"),Not(BooleanVariable("c")))))
        println("normal:")
        println(c)
        println("nnf:")
        println(Transformations.nnf(c))
        println("cnf:")
        println(Transformations.cnf(c))
        
        val test1 = Not(Not(Not(True)))
        println("normal:")
        println(test1)
        println("nnf:")
        println(Transformations.nnf(test1))
        
        val test2 = Not(Exists(Variable("b"),ForAll(Variable("a"),True)))
        println("normal:")
        println(test2)
        println("nnf:")
        println(Transformations.nnf(test2))
        
        val test3 = And(BooleanVariable("a"), And(BooleanVariable("b"),Or(BooleanVariable("c"),And(BooleanVariable("a"),BooleanVariable("c")))))
        println("normal:")
        println(test3)
        println("cnf:")
        println(Transformations.cnf(test3))
    
        val test4 = Not(And(True,False))
        println("normal:")
        println(test4)
        println("nnf:")
        println(Transformations.nnf(test4))   
        
        
        println()
        
        val a2 = True
        println("normal:")
        println(a2)
        println("simple:")
        println(Transformations.simplify(a2))
        
        val b2 = Or(And(BooleanVariable("a"),BooleanVariable("b")),True)
        println("normal:")
        println(b2)
        println("simple:")
        println(Transformations.simplify(b2))
        
        val c2 = And(BooleanVariable("a"),Or(BooleanVariable("b"),True))
        println("normal:")
        println(c2)
        println("simple:")
        println(Transformations.simplify(c2)) 
        
        val test5 = Or(And(BooleanVariable("a"),BooleanVariable("b")),False)
        println("normal:")
        println(test5)
        println("simple:")
        println(Transformations.simplify(test5)) 
        
        
        println("normal:")
        println(a)
        println("simple:")
        println(Transformations.simplify(a)) 
        
        println("normal:")
        println(b)
        println("simple:")
        println(Transformations.simplify(b)) 
        
        println("normal:")
        println(c)
        println("simple:")
        println(Transformations.simplify(c)) 
    }
}


